structure Transp =
struct
  structure Asm = Assem
  structure A = Assert
  structure Ast = Ir
  structure E = Env4Ir

  fun mapToAddr (id) = 0 (* cheat compiler! *)
  fun transLval lval infunc env senv (st:A.state) =
      let fun trans (Ast.Var(id, pos))= 
              let val  aaa = E.lookup id env
                  val (islocal, offset, types) = 
                      case aaa
                       of SOME(v) => v
                        | NONE => raise Fail "no this case, compiler bug\n"
              in  if islocal 
                  then let val roff = if infunc 
                                      then A.Plus(A.Sel(#1 st, A.Ebp), A.IntNum(offset))
                                      else A.Plus(A.Sel(#1 st, A.Esp), A.IntNum(offset-4))
                       in  (fn E.Simple => (A.Sel(#2 st, roff), types)
			     | (E.Pointer(tp')) => (A.Sel(#2 st, roff), types)
			     | _ => (roff, types)) types
                       end
                  else (fn E.Simple => (A.Sel(#2 st, A.Addr(mapToAddr(id))), types)
			 | (E.Pointer(tp')) => (A.Sel(#2 st, A.Addr(mapToAddr(id))), types)
			 | _ => (A.Addr(mapToAddr(id)), types)) types
              end
            | trans (Ast.Ptr(tp, lval, pos)) = 
              let val (exp, types) = transLval lval infunc env senv st
                  val rettype = case types
                                 of  E.Pointer(subtype) => subtype
                                   | _ => (raise Fail "impossible"; E.Simple)
              in  (fn E.Simple => (A.Sel(#2 st, exp), rettype)
		    | (E.Pointer(tp')) => (A.Sel(#2 st, exp), rettype)
		    | _ => (exp, rettype)) rettype
              end
            | trans (Ast.Inarray(lval, exp, s_array, pos)) = 
              let val (base, types) = transLval lval infunc env senv st
                  val rettype = case types 
                                 of  E.Array(_, subtype) => subtype
                                   | _ => (raise Fail "impossible"; E.Simple)
                  val elemSize = E.calTypeSize rettype senv
                  val index = transExp exp infunc env senv st
                  val offset = A.Times(index, A.IntNum(elemSize))
              in (fn E.Simple => (A.Sel(#2 st, A.Plus(base, offset)), rettype)
		   | (E.Pointer(tp')) => (A.Sel(#2 st, A.Plus(base, offset)), rettype)
		   | _ => (A.Plus(base, offset), rettype)) rettype 
              end
            | trans (Ast.Instruct(lval, id, pos)) =
              let val (base, types) = transLval lval infunc env senv st
                  val (offset, rettype) = case types
                                           of  E.Struct(str) => Option.valOf(E.lookupF str id senv)
                                             | _ => (raise Fail "impossible"; (0, E.Simple)) 
              in (fn E.Simple => (A.Sel(#2 st, A.Plus(base, A.IntNum(offset))), rettype)
		   | E.Pointer(tp') => (A.Sel(#2 st, A.Plus(base, A.IntNum(offset))), rettype)
		   | _ => (A.Plus(base, A.IntNum(offset)), rettype)) rettype
              end
            (* The ir that we translate does not processed by Selectize, so we need not translate Sel, Upd or Sharp *)
	    | trans _ = raise Fail "bug\n"
(*            | trans (Ast.Ptstruct(lval, id, pos)) =
              transLval (Ast.Instruct(Ast.Inptr(lval, pos), id, pos)) infunc env senv st*)
      in  trans lval
      end

  and transExp exp infunc env senv (st:A.state) = 
      let fun trans (Ast.IntNum(i)) = A.IntNum(i)
            | trans (Ast.Null) = A.Addr(0)
            | trans (Ast.BinopExp(e1, binop, e2, pos)) =
              let val e1' = (transExp e1 infunc env senv st)
                  val e2' = (transExp e2 infunc env senv st)
              in  case binop
                   of  Ast.Plus => A.Plus(e1', e2')
                     | Ast.Minus => A.Minus(e1', e2')
                     | Ast.Times => A.Times(e1', e2')
                     (* Div and Modus should not appear in a Prop.*)
                     | _ => (raise Fail "impossible"; A.Minus(e1', e2'))
              end
            | trans (Ast.Not(e, pos)) = 
              let val e' = transExp e infunc env senv st
              in  (raise Fail "impossible"; A.Minus(A.IntNum(0), e'))
              end
(*            | trans (Ast.NotExp(e, pos)) = 
              let val e' = transExp e infunc env senv st
              in  (raise Fail "impossible"; A.Minus(A.IntNum(0), e'))
              end*)
            | trans (Ast.Result) = A.Sel(#1 st, A.Eax)
(*            | trans (Ast.Prev(lval, pos)) = #1 (transLval lval infunc env senv st) *)
            | trans (Ast.Lval(lval)) = #1 (transLval lval infunc env senv st)
            | trans _ = (raise Fail "impossible"; A.IntNum(0))
      in  trans exp
      end 
  fun transProp exp infunc env senv st =
      let fun trans Ast.True = A.True
            | trans Ast.False = A.Not(A.True)
            | trans (Ast.BinopExp(e1, binop, e2, pos)) =
              (case binop
                of  Ast.Band => 
                    A.And(transProp e1 infunc env senv st, transProp e2 infunc env senv st)
                  | Ast.Bor =>
                    A.Or(transProp e1 infunc env senv st, transProp e2 infunc env senv st)
                  | Ast.GT =>
                    A.Gt(transExp e1 infunc env senv st, transExp e2 infunc env senv st)
                  | Ast.GE =>
                    A.Ge(transExp e1 infunc env senv st, transExp e2 infunc env senv st)
                  | Ast.LT =>
                    A.Lt(transExp e1 infunc env senv st, transExp e2 infunc env senv st)
                  | Ast.LE =>
                    A.Le(transExp e1 infunc env senv st, transExp e2 infunc env senv st)
                  | Ast.Equ =>
                    A.Eq(transExp e1 infunc env senv st, transExp e2 infunc env senv st)
                  | Ast.NEqu =>
                    A.Ne(transExp e1 infunc env senv st, transExp e2 infunc env senv st)
                  | _ => (raise Fail "impossible"; A.True))
            | trans (Ast.Not(e, pos)) = A.Not(transProp e infunc env senv st)
(*            | trans (Ast.NotExp(e, pos)) = A.Not(transProp e infunc env senv st)*)
            | trans (Ast.Imply(e1, e2, pos)) =
              A.Imply(transProp e1 infunc env senv st, transProp e2 infunc env senv st)
(*            | trans (Ast.Iff(e1, e2, pos)) =
              let val p1 = transProp e1 infunc env senv st
                  val p2 = transProp e2 infunc env senv st
              in  A.And(A.Imply(p1,p2), A.Imply(p2, p1))
              end*)
            | trans _ = (raise Fail "impossible"; A.True)
      in  trans exp
      end
(*
  fun reg2exp(reg) = 
      let fun handlereg(Asm.Eax) = A.Eax
	    | handlereg(Asm.Ebx) = A.Ebx
	    | handlereg(Asm.Ecx) = A.Ecx
	    | handlereg(Asm.Edx) = A.Edx
	    | handlereg(Asm.Esi) = A.Esi
	    | handlereg(Asm.Edi) = A.Edi
	    | handlereg(Asm.Esp) = A.Esp
	    | handlereg(Asm.Ebp) = A.Ebp
      in handlereg(reg)
      end
*)
(* WIP
  fun findcode(label,instrs) = instrs 

  val crtcode: Asm.instr list ref = ref []
  val crtfname = ref ""
  fun findspec(label) = 
      let fun corefun(A.Rf,A.Hp) = A.True
	    | corefun(_) = A.True
      in corefun
      end

  fun findprec(fid) = 
      let fun corefun(A.Rf,A.Hp) = A.True
	    | corefun(_) = A.True
      in corefun
      end

  fun findpostc(fid) = 
      let fun corefun(A.Rf,A.Hp) = A.True
	    | corefun(_) = A.True
      in corefun
      end
*)
(* update State: state*instr-> state *)
(*
  fun upState st instr = 
      let fun rf(state:A.state) = #1 state
	  fun hp(state:A.state) = #2 state
	  fun mchinstr(Asm.Addr(r1,r2)) = 
	      let val updexp2 = A.Plus(A.Sel(rf(st),reg2exp(r2)),
				       A.Sel(rf(st),reg2exp(r1)))
		  val st' = (A.Upd(rf(st),reg2exp(r2),updexp2),hp(st))
	      in st'
	      end
	    | mchinstr(Asm.Addz(imm,r2)) = 
	      let val updexp2 = A.Plus(A.Sel(rf(st),reg2exp(r2)),
				       A.IntNum(imm))
		  val st' = (A.Upd(rf(st),reg2exp(r2),updexp2),hp(st))
	      in st'
	      end
	    | mchinstr(Asm.Subr(r1,r2)) = 
	      let val updexp2 = A.Minus(A.Sel(rf(st),reg2exp(r2)),
				       A.Sel(rf(st),reg2exp(r1)))
		  val st' = (A.Upd(rf(st),reg2exp(r2),updexp2),hp(st))
	      in st'
	      end
	    | mchinstr(Asm.Subz(imm,r2)) = 
	      let val updexp2 = A.Minus(A.Sel(rf(st),reg2exp(r2)),
				       A.IntNum(imm))
		  val st' = (A.Upd(rf(st),reg2exp(r2),updexp2),hp(st))
	      in st'
	      end
	    | mchinstr(Asm.Mulr(r1,r2)) = 
	      let val updexp2 = A.Times(A.Sel(rf(st),reg2exp(r2)),
				       A.Sel(rf(st),reg2exp(r1)))
		  val st' = (A.Upd(rf(st),reg2exp(r2),updexp2),hp(st))
	      in st'
	      end
	    | mchinstr(Asm.Mulz(imm,r2)) = 
	      let val updexp2 = A.Times(A.Sel(rf(st),reg2exp(r2)),
				       A.IntNum(imm))
		  val st' = (A.Upd(rf(st),reg2exp(r2),updexp2),hp(st))
	      in st'
	      end
	    | mchinstr(Asm.Push(r1)) = 
	      let val rfupdexp2 = A.Minus(A.Sel(rf(st),A.Esp),A.IntNum(4))
		  val rf' = A.Upd(rf(st),A.Esp,rfupdexp2)
		  val hp' = A.Upd(hp(st),A.Sel(rf(st),A.Esp),
				  A.Sel(rf(st),reg2exp(r1)))
		  val st' = (rf',hp')
	      in st'
	      end
	    | mchinstr(Asm.Pop(r1)) = 
	      let val updesp = A.Upd(rf(st), A.Esp,
				     A.Plus(A.Sel(rf(st),A.Esp),A.IntNum(4)))
		  val rf' = A.Upd(updesp,reg2exp(r1),
				  A.Sel(hp(st),A.Sel(rf(st),A.Esp)))
		  val st' = (rf',hp(st))
	      in st'
	      end
	    | mchinstr(Asm.Xchg(r1,r2)) = 
	      let val rf1 = A.Upd(rf(st),reg2exp(r1),A.Sel(rf(st),reg2exp(r2)))
		  val st' = (A.Upd(rf1,reg2exp(r2),A.Sel(rf(st),reg2exp(r1))),hp(st))
	      in st'
	      end
	    | mchinstr(Asm.Leal(str,r1)) = 
	      let val st' = (A.Upd(rf(st),reg2exp(r1),A.Addr(mapToAddr(str))),hp(st))
	      in st'
	      end
	    | mchinstr(Asm.Leab(ofaddr,r1,r2)) = 
	      let val addr = A.Plus(A.Sel(rf(st),reg2exp(r1)),
				    A.IntNum(ofaddr))
		  val st' = (A.Upd(rf(st),reg2exp(r2),addr),hp(st))
	      in st'
	      end
	    | mchinstr(Asm.Movr(r1,r2)) = 
	      let val st' = (A.Upd(rf(st),reg2exp(r2),A.Sel(rf(st),reg2exp(r1)))
			     ,hp(st))
	      in st'
	      end
	    | mchinstr(Asm.Movz(imm,r2)) = 
	      let val st' = (A.Upd(rf(st),reg2exp(r2),A.IntNum(imm)),hp(st))
	      in st'
	      end
	    | mchinstr(Asm.Movld(imm,r1,r2)) = 
	      let val updexp1 = A.Sel(hp(st),A.Plus(A.Sel(rf(st),reg2exp(r1)),
						    A.IntNum(imm)))
		  val st' = (A.Upd(rf(st),reg2exp(r2),updexp1),hp(st))
	      in st'
	      end
	    | mchinstr(Asm.Movst(r1,imm,r2)) = 
	      let val updexp1 = A.Plus(A.Sel(rf(st),reg2exp(r2)),A.IntNum(imm))
		  val hp' = A.Upd(hp(st),updexp1,A.Sel(rf(st),reg2exp(r1)))
		  val st' = (rf(st),hp')
	      in st'
	      end
	    | mchinstr(_) = st
      in mchinstr(instr)
      end
*)
(* recommend not to delete the following code, maybe used later!!!
  fun upState emit instr st = 
      let fun rf(state:A.state) = #1 state
	  fun hp(state:A.state) = #2 state
	  fun mchinstr([]) = A.True
	    | mchinstr(Asm.Addr(r1,r2)::Is) = 
	      let val updexp2 = A.Plus(A.Sel(rf(st),reg2exp(r2)),
				       A.Sel(rf(st),reg2exp(r1)))
		  val st' = (A.Upd(rf(st),reg2exp(r2),updexp2),hp(st))
	      in upState emit Is st'
	      end
	    | mchinstr(Asm.Addz(imm,r2)::Is) = 
	      let val updexp2 = A.Plus(A.Sel(rf(st),reg2exp(r2)),
				       A.IntNum(imm))
		  val st' = (A.Upd(rf(st),reg2exp(r2),updexp2),hp(st))
	      in upState emit Is st'
	      end
	    | mchinstr(Asm.Subr(r1,r2)::Is) = 
	      let val updexp2 = A.Minus(A.Sel(rf(st),reg2exp(r2)),
				       A.Sel(rf(st),reg2exp(r1)))
		  val st' = (A.Upd(rf(st),reg2exp(r2),updexp2),hp(st))
	      in upState emit Is st'
	      end
	    | mchinstr(Asm.Subz(imm,r2)::Is) = 
	      let val updexp2 = A.Minus(A.Sel(rf(st),reg2exp(r2)),
				       A.IntNum(imm))
		  val st' = (A.Upd(rf(st),reg2exp(r2),updexp2),hp(st))
	      in upState emit Is st'
	      end
	    | mchinstr(Asm.Mulr(r1,r2)::Is) = 
	      let val updexp2 = A.Times(A.Sel(rf(st),reg2exp(r2)),
				       A.Sel(rf(st),reg2exp(r1)))
		  val st' = (A.Upd(rf(st),reg2exp(r2),updexp2),hp(st))
	      in upState emit Is st'
	      end
	    | mchinstr(Asm.Mulz(imm,r2)::Is) = 
	      let val updexp2 = A.Times(A.Sel(rf(st),reg2exp(r2)),
				       A.IntNum(imm))
		  val st' = (A.Upd(rf(st),reg2exp(r2),updexp2),hp(st))
	      in upState emit Is st'
	      end
	    | mchinstr(Asm.Push(r1)::Is) = 
	      let val rfupdexp2 = A.Minus(A.Sel(rf(st),A.Esp),A.IntNum(4))
		  val rf' = A.Upd(rf(st),A.Esp,rfupdexp2)
		  val hp' = A.Upd(hp(st),A.Sel(rf(st),A.Esp),
				  A.Sel(rf(st),reg2exp(r1)))
		  val st' = (rf',hp')
	      in upState emit Is st'
	      end
	    | mchinstr(Asm.Pop(r1)::Is) = 
	      let val updesp = A.Upd(rf(st), A.Esp,
				     A.Plus(A.Sel(rf(st),A.Esp),A.IntNum(4)))
		  val rf' = A.Upd(updesp,reg2exp(r1),
				  A.Sel(hp(st),A.Sel(rf(st),A.Esp)))
		  val st' = (rf',hp(st))
	      in upState emit Is st'
	      end
	    | mchinstr(Asm.Cmpr(r1,r2)::Is) = 
	      let val rf1' = A.Upd(rf(st),A.Zf,A.IntNum(1))
		  val st1' = (A.Upd(rf1',A.Sf,A.IntNum(0)),hp(st))
		  val rf2' = A.Upd(rf(st),A.Zf,A.IntNum(0))
		  val st2' = (A.Upd(rf2',A.Sf,A.IntNum(0)),hp(st))
		  val rf3' = A.Upd(rf(st),A.Zf,A.IntNum(0))
		  val st3' = (A.Upd(rf3',A.Sf,A.IntNum(1)),hp(st))
		  val nwprop' = A.And(A.Imply(A.Gt(A.Sel(rf(st),reg2exp(r2)),
						   A.Sel(rf(st),reg2exp(r1))),
					      upState emit Is st2'),
				      A.Imply(A.Lt(A.Sel(rf(st),reg2exp(r2)),
						   A.Sel(rf(st),reg2exp(r1))),
					      upState emit Is st3'))
		  val nwprop = A.And(A.Imply(A.Eq(A.Sel(rf(st),reg2exp(r2)),
						   A.Sel(rf(st),reg2exp(r1))),
					      upState emit Is st1'),
				     nwprop')
	      in nwprop
	      end
	    | mchinstr(Asm.Cmpz(imm,r2)::Is) = 
	      let val rf1' = A.Upd(rf(st),A.Zf,A.IntNum(1))
		  val st1' = (A.Upd(rf1',A.Sf,A.IntNum(0)),hp(st))
		  val rf2' = A.Upd(rf(st),A.Zf,A.IntNum(0))
		  val st2' = (A.Upd(rf2',A.Sf,A.IntNum(0)),hp(st))
		  val rf3' = A.Upd(rf(st),A.Zf,A.IntNum(0))
		  val st3' = (A.Upd(rf3',A.Sf,A.IntNum(1)),hp(st))
		  val nwprop' = A.And(A.Imply(A.Gt(A.Sel(rf(st),reg2exp(r2)),
						   A.IntNum(imm)),
					      upState emit Is st2'),
				      A.Imply(A.Lt(A.Sel(rf(st),reg2exp(r2)),
						   A.IntNum(imm)),
					      upState emit Is st3'))
		  val nwprop = A.And(A.Imply(A.Eq(A.Sel(rf(st),reg2exp(r2)),
						   A.IntNum(imm)),
					      upState emit Is st1'),
				     nwprop')
	      in nwprop
	      end
	    | mchinstr(Asm.Xchg(r1,r2)::Is) = 
	      let val rf1 = A.Upd(rf(st),reg2exp(r1),A.Sel(rf(st),reg2exp(r2)))
		  val st' = (A.Upd(rf1,reg2exp(r2),A.Sel(rf(st),reg2exp(r1))),hp(st))
	      in upState emit Is st'
	      end
	    | mchinstr(Asm.Leal(str,r1)::Is) = 
	      let val st' = (A.Upd(rf(st),reg2exp(r1),A.Addr(mapToAddr(str))),hp(st))
	      in upState emit Is st'
	      end
	    | mchinstr(Asm.Leab(ofaddr,r1,r2)::Is) = (*WIP*)
	      let val addr = A.Plus(A.Sel(rf(st),reg2exp(r1)),
				    A.IntNum(ofaddr))
		  val st' = (A.Upd(rf(st),reg2exp(r2),addr),hp(st))
	      in upState emit Is st'
	      end
	    | mchinstr(Asm.Movr(r1,r2)::Is) = 
	      let val st' = (A.Upd(rf(st),reg2exp(r2),A.Sel(rf(st),reg2exp(r1)))
			     ,hp(st))
	      in upState emit Is st'
	      end
	    | mchinstr(Asm.Movz(imm,r2)::Is) = 
	      let val st' = (A.Upd(rf(st),reg2exp(r2),A.IntNum(imm)),hp(st))
	      in upState emit Is st'
	      end
	    | mchinstr(Asm.Movld(imm,r1,r2)::Is) = 
	      let val updexp1 = A.Sel(hp(st),A.Plus(A.Sel(rf(st),reg2exp(r1)),
						    A.IntNum(imm)))
		  val st' = (A.Upd(rf(st),reg2exp(r2),updexp1),hp(st))
	      in upState emit Is st'
	      end
	    | mchinstr(Asm.Movst(r1,imm,r2)::Is) = 
	      let val updexp1 = A.Plus(A.Sel(rf(st),reg2exp(r2)),A.IntNum(imm))
		  val hp' = A.Upd(hp(st),updexp1,A.Sel(rf(st),reg2exp(r1)))
		  val st' = (rf(st),hp')
	      in upState emit Is st'
	      end
	    | mchinstr(Asm.Je(lb)::Is) = 
	      let val jumpForward = true
		  val tbr = A.And(A.Imply(A.Ne(A.Sel(rf(st),A.Zf),A.IntNum(0)),
					  upState emit Is st),
				  A.Imply(A.Eq(A.Sel(rf(st),A.Zf),A.IntNum(0)),
					  upState emit (findcode(lb,Is)) st))
		  val newvc = A.Imply(A.Eq(A.Sel(rf(st),A.Zf),A.IntNum(0)),
				      findspec(lb)(st))
		  val fbr = A.Imply(A.Ne(A.Sel(rf(st),A.Zf),A.IntNum(0)),
				    upState emit Is st)
	      in if jumpForward
		 then tbr
		 else (emit(newvc);fbr)
	      end
	    | mchinstr(Asm.Jge(lb)::Is) = 
	      let val jumpForward = true
		  val cond1 = A.Or(A.Eq(A.Sel(rf(st),A.Zf),A.IntNum(1)),
				   A.Eq(A.Sel(rf(st),A.Sf),A.IntNum(0)))
		  val cond2 = A.Not(cond1)
		  val tbr = A.And(A.Imply(cond2, upState emit Is st),
				  A.Imply(cond1, upState emit (findcode(lb,Is)) st))
		  val newvc = A.Imply(cond1, findspec(lb)(st))
		  val fbr = A.Imply(cond2, upState emit Is st)
	      in if jumpForward
		 then tbr
		 else (emit(newvc);fbr)
	      end
	    | mchinstr(Asm.Jg(lb)::Is) = 
	      let val jumpForward = true
		  val cond1 = A.And(A.Eq(A.Sel(rf(st),A.Zf),A.IntNum(0)),
				    A.Eq(A.Sel(rf(st),A.Sf),A.IntNum(0)))
		  val cond2 = A.Not(cond1)
		  val tbr = A.And(A.Imply(cond2, upState emit Is st),
				  A.Imply(cond1, upState emit (findcode(lb,Is)) st))
		  val newvc = A.Imply(cond1, findspec(lb)(st))
		  val fbr = A.Imply(cond2, upState emit Is st)
	      in if jumpForward
		 then tbr
		 else (emit(newvc);fbr)
	      end
	    | mchinstr(Asm.Jmp(lb)::Is) = 
	      let val jumpForward = true
		  val newvc = findspec(lb)(st)
	      in if jumpForward
		 then upState emit (findcode(lb,Is)) st
		 else (emit(newvc);A.True)
	      end
	    | mchinstr(Asm.Call(fname)::Is) = 
	      let val newvc = findprec(fname)(st)
	      in (emit(newvc);
		  VCgen (findpostc(fname)) Is st;
		  A.True)
	      end
	    | mchinstr(Asm.Ret::Is) = 
	      let val newvc = findpostc(!crtfname)(st)
	      in (emit(newvc);A.True)
	      end
	    | mchinstr(Asm.Label(lbname,assop)::Is) = 
	      let fun check(SOME(pa)) = pa
		    | check(NONE) = 
		      let fun corefunc(A.Rf,A.Hp) = A.True
			    | corefunc(_) = A.True
		      in corefunc
		      end
		  val assop' = check(assop)
		  val newvc = assop' st
	      in (emit(newvc);
		  VCgen assop' Is st;
		  A.True)
	      end
	    | mchinstr(_) = A.True
      in mchinstr(instr)
      end
  and VCgen inv instr st = 
      let val vcs = ref []
	  fun emit prop = 
	      let val newprop = A.Imply(inv st, prop)
	      in vcs := newprop::(!vcs)
	      end
	  val _ = upState emit instr st
      in ()
      end
*)
end
